COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	The new work of the Formal Reasoning Group is based on exploiting
C00006 ENDMK
C⊗;
The new work of the Formal Reasoning Group is based on exploiting
some discoveries made in the last year and a half.  These discoveries
are:

1. McCarthy has discovered how to represent in first order logic
information formerly considered to require modal logic for its
expression.  This work is embodied in the forthcoming report
%2First Order Theories of Individual Concepts%1.  The significance
of the discovery is that facts about who knows what, believes what,
and wants what can be expressed without extending first order logic.
Therefore, the laws governing these notions are ordinary axioms and
can be readily changed and experimented with.

	Here is an example of one of the well-known problems and
its resolution in our new system.  Consider the sentence, %2"The
Russians believe they know the speed of the Trident submarine"%1.
For computer manipulation this sentence is usually represented
internally in some such form as

	(BELIEVES RUSSIANS (KNOW RUSSIANS (SPEED TRIDENT))).

This internal representation may result either from a program that
reads the English sentence or it may be entered directly according
to what aspect of the problem is being studied.
Such a sentence in the memory of a computer is useful only if it can
be used to draw conclusions, and the rules that permit drawing conclusions
should allow correct conclusions and not allow incorrect ones.
One of the most powerful rules of inference is the substitution of
equals for equals.  Thus someone has concluded that
the Russians are the employers of someone designated as %2spy3%1, the
data base might acquire the sentence above sentence from the sentences

	(EQUAL RUSSIANS (EMPLOYERS SPY3))

and the sentence

	(BELIEVES SPY3 (KNOW SPY3 (SPEED TRIDENT))).

and suitably expressed general laws about what spies tell their employers.

However, there is a well known pitfall in reasoning about belief and
knowledge.  Suppose that (SPEED TRIDENT) is the same as the speed of
the Russian submarine XXX.  The the above sentence should not follow
from the sentence

	(BELIEVE RUSSIANS (KNOW RUSSIANS (SPEED XXX)))

unless we also have a hypothesis to the effect that the Russians believe
the two submarines have the same speed.

	Thus we can sometimes substitute equals for equals but not
always.  The contexts in which it is not legitimate to substitute
equals for equals are called %2opaque contexts%1, and it has been
necessary to modify the logic in order to treat them.